\begin{tabbing}
$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), ${\it es}$:ES, $x$:Id, $e$:\{$e$:E$\mid$ @loc($e$)($x$:$T$)\} .
\\[0ex]($\neg$($\uparrow$first($e$)))
\\[0ex]$\Rightarrow$ ($\uparrow$discrete(loc($e$);$x$))
\\[0ex]$\Rightarrow$ (($x$ when pred($e$)) = ($x$ when $e$) $\in$ $T$)
\\[0ex]$\Rightarrow$ \=($x$ changed before pred($e$) = $x$ changed before $e$ $\in$ $\mathbb{B}$\+
\\[0ex]\& (\=($\uparrow$$x$ changed before $e$)\+
\\[0ex]$\Rightarrow$ ((last change to $x$ before $e$) = (last change to $x$ before pred($e$)) $\in$ E)))
\-\-
\end{tabbing}